s:POSet{i}, a, b:|s|. (a  b)  ((a <s b)  (a = b)) 

latex

Up	sets 1
Definitions of Statement	PosetSig, DSet, QOSet, POSet{i}
Definitions	t  T, x:A. B(x), P & Q, x,y. t(x;y), P  Q, , P  Q, P  Q, P  Q, anti_sym(T;R), trans(T;E), refl(T;E), x,y:T. E(x;y), order(T;R), E\, DSet, QOSet, POSet{i}, x(s1,s2), Preorder(T;x,y.R(x;y))
Lemmas	poset wf, set car wf, decidable dset eq, xxorder split, set lt wf, s part wf, set leq wf, ab binrel wf, iff functionality wrt iff, set eq wf, eqfun p wf, poset sig wf, dset properties, preorder wf, dset wf, qoset properties, anti sym wf, qoset wf, poset properties, set lt is sp of leq a, or functionality wrt iff, not wf